(*
 * Copyright (c) 2009, Palle Raabjerg
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 *   * Redistributions of source code must retain the above copyright notice,
 *     this list of conditions and the following disclaimer.
 *   * Redistributions in binary form must reproduce the above copyright notice,
 *     this list of conditions and the following disclaimer in the documentation
 *     and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 * POSSIBILITY OF SUCH DAMAGE.
 *)

(* Simple OCaml wrapper to the Succinct Solver. *)

(*#load "unix.cma";;
#load "str.cma";;*)
(* open Spitree;;*)
(*#load "alfp.cmo";;
#load "outputparser.cmo";;
#load "outputlexer.cmo";;*)

open Alfp;;

(* Execute system command.
 * Found on the http://www.rosettacode.org wiki.
 * Saved the trouble figuring it out myself. Thanks!
 * Only modified slightly to allow for stdin input.
 * According to
 * http://caml.inria.fr/pub/docs/manual-ocaml/manual035.html
 * Unix.open_process and Unix.close_process are both fully
 * implemented in the Windows version of OCaml. So with
 * any luck, that shouldn't cause too many problems.
 * Input:
 * string cmd - Command to be executed.
 * string stdinput - Standard input for the command.
 * Output: string - Resulting stdout of command. *)
let syscall cmd stdinput =
  let inc, outc = Unix.open_process cmd in
    output_string outc stdinput;
    close_out outc;
  let buf = Buffer.create 16 in
    (try
       while true do
	 Buffer.add_channel buf inc 1
       done
     with End_of_file -> ());
    let _status = Unix.close_process (inc, outc) in
      Buffer.contents buf;;

let preds_of_list relation rellist =
  List.map (fun termlist ->
	      CPredicate(relation, termlist)
	   ) rellist;;

let list_of_result relmap =
  SMap.fold (fun relation rellist accumlist ->
	       List.append (preds_of_list relation rellist) accumlist
	    ) relmap [];;

exception OnlyCPredicates of string;;
let filter_essential rellist =
  List.filter (fun pred ->
		 match pred with
		   | CPredicate(relation, _) ->
		       let regex = Str.regexp ".+[-][0-9]+" in
			 not (Str.string_match regex relation 0)
		   | _ -> true) rellist


let deducible_facts clause ssheap =
  let cl_string = string_of_cl clause in
    (*print_endline cl_string;*)
  let fact_string = syscall ("sml @SMLload=" ^ ssheap) cl_string in
    (*print_endline ("Deducible facts:\n" ^ fact_string);*)
  let lexbuf = Lexing.from_string (fact_string ^ "#") in
  let facts = Outputparser.output Outputlexer.out_tokens lexbuf in
    list_of_result facts;;

(*let listing = syscall "sml @SMLload=heap" "(A U.fmember(U) => factivity(U)) & (A V.A U.treo(V) & deposit(U,V) => fmember(U)) & treo(markus) & deposit(palle, markus)";;
print_endline listing;;

let listing = listing ^ "#" (* Ending token. For the benefit of the parser. *)

let lexbuf = Lexing.from_string listing;;
let solverresult = Outputparser.output Outputlexer.out_tokens lexbuf;;

let resultlist = list_of_result solverresult;;

let essentials = filter_essential resultlist;;*)



(* Parse a sample *)
(* let infile = Sys.argv.(1) *)
(*let infile = "datsamples/fklub.dat";;*)

(*let filechan = open_in infile;;
let lexbuf = Lexing.from_channel filechan;;

let datprog = Spiparser.dprogram Spilexer.spi_tokens lexbuf;;

let fact:hclause = [("factivity", [SpiMsg(Name("palle"))])];;*)

(*print_endline ((string_of_hclause fact) ^ "\n");
print_endline ((string_of_datalog datprog) ^ "\n");;*)

(*let result = query datprog fact;;*)
